home *** CD-ROM | disk | FTP | other *** search
/ Garbo / Garbo.cdr / mac / progrmng / cmlmcmpw.sit / Caml Light / examples / kb / terms.ml < prev   
Encoding:
Text File  |  1991-05-23  |  3.1 KB  |  109 lines  |  [TEXT/MPS ]
  1. (****************** Term manipulations *****************)
  2.  
  3. #open "prelude";;
  4.  
  5. type term = Var of int
  6.           | Term of string * term list;;
  7.  
  8. let rec vars = function
  9.     Var n -> [n]
  10.   | Term(_,L) -> vars_of_list L
  11. and vars_of_list = function
  12.     [] -> []
  13.   | t::r -> union (vars t) (vars_of_list r)
  14. ;;
  15.  
  16. let substitute subst = subst_rec where rec subst_rec = function
  17.     Term(oper,sons) -> Term(oper, map subst_rec sons)
  18.   | Var(n) as t     -> try assoc n subst with failure _ -> t
  19. ;;
  20.  
  21. let change f = change_rec where rec change_rec =
  22.   fun (h::t) n -> (* print_int n; print_string "\n"; *)
  23.                   if n=1 then f h :: t else h :: change_rec t (n-1)
  24.    |    _    _ -> failwith "change"
  25. ;;
  26.  
  27. (* Term replacement replace M u N => M[u<-N] *)
  28. let replace M u N = reprec(M,u)
  29.   where rec reprec = function
  30.     _, [] -> N
  31.   | Term(oper,sons), (n::u) ->
  32.              Term(oper, change (fun P -> reprec(P,u)) sons n)
  33.   | _ -> failwith "replace"
  34. ;;
  35.  
  36. (* matching = - : (term -> term -> subst) *)
  37. let matching term1 term2 =
  38.   let rec match_rec subst = function
  39.       Var v, M ->
  40.         if mem_assoc v subst then
  41.           if M = assoc v subst then subst else failwith "matching"
  42.         else
  43.           (v,M) :: subst
  44.     | Term(op1,sons1), Term(op2,sons2) ->
  45.     if op1 = op2 then it_list2 match_rec subst sons1 sons2
  46.                      else failwith "matching"
  47.     | _ -> failwith "matching" in
  48.   match_rec [] (term1,term2)
  49. ;;
  50.  
  51. (* A naive unification algorithm *)
  52.  
  53. let compsubst subst1 subst2 = 
  54.   (map (fun (v,t) -> (v, substitute subst1 t)) subst2) @ subst1
  55. ;;
  56.  
  57. let occurs n = occur_rec where rec occur_rec = function
  58.     Var m -> m=n
  59.   | Term(_,sons) -> exists occur_rec sons
  60. ;;
  61.  
  62. let rec unify = function
  63.     (Var n1 as term1), term2 ->
  64.       if term1 = term2 then []
  65.       else if occurs n1 term2 then failwith "unify1"
  66.       else [n1,term2]
  67.   | term1, Var n2 ->
  68.       if occurs n2 term1 then failwith "unify2"
  69.       else [n2,term1]
  70.   | Term(op1,sons1), Term(op2,sons2) ->
  71.       if op1 = op2 then 
  72.     it_list2 (fun s (t1,t2) -> compsubst (unify(substitute s t1,
  73.                                                     substitute s t2)) s)
  74.                  [] sons1 sons2
  75.       else failwith "unify3"
  76. ;;
  77.  
  78. (* We need to print terms with variables independently from input terms
  79.   obtained by parsing. We give arbitrary names v1,v2,... to their variables. *)
  80.  
  81. let INFIXES = ["+";"*"];;
  82.  
  83. let rec pretty_term = function
  84.     Var n ->
  85.       print_string "v"; print_int n
  86.   | Term (oper,sons) ->
  87.       if mem oper INFIXES then
  88.         match sons with
  89.             [s1;s2] ->
  90.               pretty_close s1; print_string oper; pretty_close s2
  91.           | _ ->
  92.               failwith "pretty_term : infix arity <> 2"
  93.       else
  94.        (print_string oper;
  95.         match sons with
  96.          []   -> ()
  97.           | t::lt -> print_string "(";
  98.                      pretty_term t;
  99.                      do_list (fun t -> print_string ","; pretty_term t) lt;
  100.                      print_string ")")
  101. and pretty_close = function
  102.     Term(oper, _) as M ->
  103.       if mem oper INFIXES then
  104.         (print_string "("; pretty_term M; print_string ")")
  105.       else pretty_term M
  106.   | M -> pretty_term M
  107. ;;
  108.  
  109.